// Copyright 2019 - University of Strathclyde, King's College London and Schlumberger Ltd
// This source code is licensed under the BSD license found in the LICENSE file in the root directory of this source tree.

#include "Events.h"
#include "Action.h"
#include "Plan.h"
#include "RobustAnalyse.h"
#include "Validator.h"

namespace VAL {

  Events::Events(const operator_list *ops)
      : ungroundEvents(),
        ungroundProcesses(),
        triggeredEvents(),
        triggeredProcesses(),
        untriggeredProcesses(),
        activeProcesses(),
        eventsForMutexCheck(),
        oldTriggeredEvents(),
        lastHappeningTime(0),
        ctsEventTriggered(false)  //, noevents(0)
  {
    for (operator_list::const_iterator i = ops->begin(); i != ops->end(); ++i) {
      if (event *e = dynamic_cast< event * >(*i)) {
        ungroundEvents.push_back(e);
      } else if (process *p = dynamic_cast< process * >(*i)) {
        ungroundProcesses.push_back(p);
      };
    };
  };

  Events::~Events() {
    ungroundEvents.clear();
    triggeredEvents.clear();
    ungroundProcesses.clear();
    triggeredProcesses.clear();
    for (vector< const Action * >::iterator i = oldTriggeredEvents.begin();
         i != oldTriggeredEvents.end(); ++i)
      delete *i;

    for (map< const StartAction *,
              pair< const Proposition *, const_symbol_list * > >::iterator j =
             activeProcesses.begin();
         j != activeProcesses.end(); ++j) {
      j->second.first->destroy();
      delete j->second.second;
    };

    activeProcesses.clear();
  };

  string Events::getName(operator_ *op, const_symbol_list *csl) const {
    string eventName = "(" + op->name->getName();
    for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
         ++cs) {
      eventName += " " + (*cs)->getName();
    };

    return eventName + ")";
  };

  bool Events::isTriggered(event *eve, const_symbol_list *csl) const {
    string eventName = eve->name->getName();
    for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
         ++cs) {
      eventName += (*cs)->getName();
    };

    set< string >::const_iterator i = triggeredEvents.find(eventName);

    if (i != triggeredEvents.end()) {
      eventName = "(" + eve->name->getName();
      for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
           ++cs) {
        eventName += " " + (*cs)->getName();
      };
      eventName += ")";

      if (LaTeX) {
        *report << "\\errorr{Attempt to trigger event \\exprn{" << eventName
                << "} twice}\\\\\n";
      } else if (Verbose)
        *report << "Attempt to trigger event " << eventName << " twice\n";

      return true;
    };

    return false;
  };

  bool Events::isTriggered(const Action *act) const {
    string eventName = act->getName0();

    set< string >::const_iterator i = triggeredEvents.find(eventName);

    if (i != triggeredEvents.end()) {
      if (LaTeX) {
        *report << "\\errorr{Attempt to trigger event \\exprn{" << *act
                << "} twice}\\\\\n";
      } else if (Verbose)
        *report << "Attempt to trigger event " << *act << " twice\n";

      return true;
    };

    return false;
  };

  bool Events::isProcessTriggered(const StartAction *sa) const {
    set< const StartAction * >::iterator i = triggeredProcesses.find(sa);

    return (i != triggeredProcesses.end());
  };

  bool Events::isProcessActive(process *pro, const_symbol_list *csl) const {
    string processName = pro->name->getName();
    for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
         ++cs) {
      processName += (*cs)->getName();
    };

    for (map< const StartAction *,
              pair< const Proposition *, const_symbol_list * > >::const_iterator
             i = activeProcesses.begin();
         i != activeProcesses.end(); ++i) {
      if (processName == i->first->getName0()) {
        return true;
      };
    };

    return false;
  };

  bool Events::isProcessUntriggered(process *pro,
                                    const_symbol_list *csl) const {
    string processName = pro->name->getName();
    for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
         ++cs) {
      processName += (*cs)->getName();
    };

    set< string >::iterator i = untriggeredProcesses.find(processName);

    return (i != untriggeredProcesses.end());
  };

  void deleteParameters(vector< const_symbol_list * > &vcsl) {
    for (vector< const_symbol_list * >::iterator p = vcsl.begin();
         p != vcsl.end(); ++p)
      delete *p;
  };

  const vector< const_symbol_list * > removeRepeatedParameters(
      const vector< const_symbol_list * > &vcsl) {
    vector< const_symbol_list * > listOfParameters;

    set< string > parameterLists;
    for (vector< const_symbol_list * >::const_iterator i = vcsl.begin();
         i != vcsl.end(); ++i) {
      string eventName;
      for (const_symbol_list::iterator cs = (*i)->begin(); cs != (*i)->end();
           ++cs) {
        eventName += (*cs)->getName();
      };

      set< string >::const_iterator pl = parameterLists.find(eventName);
      if (pl == parameterLists.end()) {
        listOfParameters.push_back(*i);
        parameterLists.insert(eventName);
      } else
        delete *i;
    };

    return listOfParameters;
  };

  const_symbol_list *newBlankConstSymbolList(var_symbol_list *parameters,
                                             Validator *v) {
    // create blank list of parameters, ie every parameter is undefined
    const_symbol_list *blankcsl = new const_symbol_list();
    for (var_symbol_list::const_iterator i = parameters->begin();
         i != parameters->end(); ++i) {
      const_symbol *cs = 0;  // v->getAnalysis()->const_tab.symbol_get("");
      blankcsl->push_back(cs);
    };

    return blankcsl;
  };

  const EndAction *addEndProcess(vector< const Action * > &processes,
                                 const StartAction *sa, const_symbol_list *csl,
                                 Validator *v) {
    // create end action to end the process
    const operator_ *pro = sa->getAction();
    action *dae = new safeaction(pro->name, pro->parameters,
                                 new conj_goal(new goal_list()),
                                 new effect_lists(), pro->symtab);
    const EndAction *endAct =
        new EndAction(v, dae, csl, sa, 0, new goal_list());
    processes.push_back(endAct);
    return endAct;
  };

  void Events::updateHappeningTime(double t) {
    if (lastHappeningTime != t) {
      triggeredEvents.clear();  // to check for events being triggered twice at
                                // the same time point
      triggeredProcesses.clear();    // to ensure a process is not triggered and
                                     // untriggered at same time point due to
                                     // rounding errors
      untriggeredProcesses.clear();  // to ensure a processes is not untriggered
                                     // and then retriggered at the same time
                                     // point due to rounding when triggering
                                     // processes by discrete change!
    };
    lastHappeningTime = t;
  };

  void Events::updateEventsForMutexCheck(Validator *v) {
    eventsForMutexCheck.clear();
    vector< const_symbol_list * > listOfParameters0;
    vector< const_symbol_list * > listOfParameters00;
    set< var_symbol * > svs;
    vector< const_symbol_list * > listOfParameters;

    for (vector< event * >::iterator e = ungroundEvents.begin();
         e != ungroundEvents.end(); ++e) {
      listOfParameters0 =
          getParametersCts((*e)->precondition, *e, v, false, true);
      listOfParameters00 = removeRepeatedParameters(listOfParameters0);
      svs = getVariables(*e);
      listOfParameters =
          defineUndefinedParameters(listOfParameters00, *e, v, svs);

      // add events to a event happening
      for (vector< const_symbol_list * >::iterator p = listOfParameters.begin();
           p != listOfParameters.end(); ++p) {
        const Action *anAction = new Action(v, *e, *p);
        eventsForMutexCheck.push_back(anAction);
        oldTriggeredEvents.push_back(anAction);
      };  // end of looping thro' parameters

      deleteParameters(listOfParameters);
    };
  };

  // trigger processes and events before the first happening in the plan
  bool Events::triggerInitialEvents(Validator *v, double firstHappeningTime) {
    if (!hasEvents()) return true;

    bool isOK = true;
    ActiveCtsEffects *ace = v->getActiveCtsEffects();
    ace->clearCtsEffects();  // clear cts effect given by the first happening

    // check for events and processes in the intitial state
    isOK = triggerDiscreteEvents(v, true);

    // update values before the first happening of the plan!
    if (ace->hasCtsEffects() &&
        (isOK || ContinueAnyway))  // if processes have been activated in the
                                   // intitial state then there may be events to
                                   // trigger and we need to update values
                                   // before the first happening
    {
      ace->setTime(firstHappeningTime);
      ace->setLocalUpdateTime(firstHappeningTime);
      isOK = triggerEventsOnInterval(v, true) && isOK;

      if (isOK || ContinueAnyway) {
        // execute cts update happening
        if (firstHappeningTime != 0) {
          if (Verbose) *report << "\n";
          ace->setLocalUpdateTime(firstHappeningTime - v->getState().getTime());
          const Happening *updateHap = ace->getCtsEffectUpdate();
          updateHap->adjustActiveCtsEffects(*ace);
          isOK = v->executeHappening(updateHap) && isOK;
          ace->ctsEffectsProcessed = false;
          ace->addActiveFEs();  // update cts effects
        };
      };
    };

    v->adjustActiveCtsEffects(ace);
    return isOK;
  };

  bool Events::triggerEventsOnInterval(Validator *v, bool init) {
    bool isOK = true;

    do {
      isOK = triggerDiscreteEvents(v, init) && isOK;
      if (!isOK && !ContinueAnyway) return false;

      isOK = triggerContinuousEvents(v, init) && isOK;
      if (!isOK && !ContinueAnyway) return false;

    } while (ctsEventTriggered);

    return isOK;
  };

  bool checkPreconditionsAreNotSatisfied(
      const State *s, const vector< const Action * > &events) {
    for (vector< const Action * >::const_iterator i = events.begin();
         i != events.end(); ++i) {
      //  cout << "Checking a precondition for "<< *i << "\n";
      if ((*i)->getPrecondition()->evaluate(s)) {
        if (LaTeX)
          *report << "\\> Event " << *i
                  << " does not falsify its precondition!\\\\\n";
        else if (Verbose)
          cout << "Event " << *i << " does not falsify its precondition!\n";

        return false;
      };
    };

    return true;
  };

  // trigger events given by discrete change
  bool Events::triggerDiscreteEvents(Validator *v, bool init) {
    if (EventPNEJuddering) JudderPNEs = true;
    double theCurrentTime = v->getState().getTime();
    updateHappeningTime(theCurrentTime);
    bool isOK = true;

    vector< const_symbol_list * > listOfParameters;
    int numberofEvents = 0;
    // trigger events: build up list of events to be triggered then add to a
    // happening and execute the happening then test for more events
    bool eventTriggered;
    do {
      eventTriggered = false;
      vector< const Action * > acts;

      for (vector< event * >::iterator e = ungroundEvents.begin();
           e != ungroundEvents.end(); ++e) {
        // cout << "Checking event\n";
        if (!init || (theCurrentTime != 0)) {
          listOfParameters =
              getParametersDiscreteFinal((*e)->precondition, *e, v->getState());
        } else {
          listOfParameters =
              getParametersDiscreteInitialFinal((*e)->precondition, *e, v);

          if (!listOfParameters.empty()) {
            *report
                << "Event preconditions are not permitted to be satisfied in "
                   "the initial state!\n";
            if (!ContinueAnyway) return false;
            isOK = false;
          };
        };

        // add events to a event happening and remove repetitions
        for (vector< const_symbol_list * >::iterator p =
                 listOfParameters.begin();
             p != listOfParameters.end(); ++p) {
          if (isTriggered(*e, *p))
            isOK = false;
          else {
            const Action *anAction = new Action(
                v, *e,
                *p);  // include precondition to check for mutex events? yes
            acts.push_back(anAction);
            triggeredEvents.insert(anAction->getName0());
            oldTriggeredEvents.push_back(anAction);
          };

        };  // end of looping thro' parameters

        deleteParameters(listOfParameters);

      };  // end of looping thro' events

      // apply events as a happening to the state
      if (acts.size() != 0 && (isOK || ContinueAnyway)) {
        if (numberofEvents > 1) {
          *report << "Event cascades of this nature are not yet handled "
                     "robustly!\n";
          if (!ContinueAnyway) return false;
          isOK = false;
        };

        if (Verbose) cout << "\n";
        Happening *eventHappening = new Happening(v, acts, true);
        isOK = v->executeHappening(eventHappening) && isOK;
        isOK =
            checkPreconditionsAreNotSatisfied(&(v->getState()), acts) && isOK;
        eventHappening->clearActions();
        delete eventHappening;
        if (!isOK && !ContinueAnyway) return false;
        eventTriggered = true;
        numberofEvents = acts.size();
      };

      isOK = triggerDiscreteProcesses(v) && isOK;

    } while (eventTriggered);  // if events were triggered this may result in
                               // more events triggering

    eventsForMutexCheck.clear();

    if (EventPNEJuddering) JudderPNEs = false;
    return isOK;
  };

  const StartAction *newStartProcessAction(process *pro, const_symbol_list *csl,
                                           Validator *v) {
    effect_lists *elc = new effect_lists();

    for (pc_list< timed_effect * >::const_iterator i =
             pro->effects->timed_effects.begin();
         i != pro->effects->timed_effects.end(); ++i) {
      if ((*i)->ts == E_CONTINUOUS) {
        insert_effects(elc, (*i)->effs);
      };
    };

    // create a StartAction here
    action *das = new safeaction(pro->name, pro->parameters,
                                 new conj_goal(new goal_list()),
                                 new effect_lists(), pro->symtab);
    return new StartAction(v, das, csl, new conj_goal(new goal_list()), elc,
                           0.0, new goal_list(),
                           vector< const CondCommunicationAction * >(),
                           vector< const CondCommunicationAction * >());
  };

  const EndAction *newEndProcess(const StartAction *sa, const_symbol_list *csl,
                                 Validator *v) {
    // create end action to end the process
    const operator_ *pro = sa->getAction();
    action *dae = new safeaction(pro->name, pro->parameters,
                                 new conj_goal(new goal_list()),
                                 new effect_lists(), pro->symtab);
    const EndAction *endAct =
        new EndAction(v, dae, csl, sa, 0, new goal_list());
    return endAct;
  };

  // trigger processes given by discrete change
  bool Events::triggerDiscreteProcesses(Validator *v) {
    if (EventPNEJuddering) JudderPNEs = true;
    bool isOK = true;
    vector< const Action * > processes;
    double time = v->getState().getTime();

    // find processes that are ended
    if (time > 0) {
      vector< const StartAction * > eraseElements;
      for (map< const StartAction *,
                pair< const Proposition *, const_symbol_list * > >::iterator
               ap = activeProcesses.begin();
           ap != activeProcesses.end(); ++ap) {
        const_cast< Proposition * >(ap->second.first)
            ->resetCtsFunctions();  // ensure we are checking the precondition
                                    // at a point not on an interval

        if (!(ap->second.first->evaluate(&v->getState())) &&
            !(isProcessTriggered(ap->first))) {
          const EndAction *endAct =
              addEndProcess(processes, ap->first, ap->second.second, v);
          oldTriggeredEvents.push_back(endAct);
          ap->second.first->destroy();
          delete ap->second.second;
          eraseElements.push_back(ap->first);
          untriggeredProcesses.insert(ap->first->getName0());
        };
      };

      for (vector< const StartAction * >::iterator ee = eraseElements.begin();
           ee != eraseElements.end(); ++ee)
        activeProcesses.erase(*ee);
    };

    for (vector< process * >::const_iterator p = ungroundProcesses.begin();
         p != ungroundProcesses.end(); ++p) {
      // for every process check if it could be triggered in the initial state
      // or later on get list of parameters  (may be empty)
      vector< const_symbol_list * > listOfParameters;
      if (time == 0.0) {
        listOfParameters =
            getParametersDiscreteInitialFinal((*p)->precondition, *p, v);
      } else {
        listOfParameters = getParametersDiscreteFinal(
            (*p)->precondition, *p,
            v->getState());  // need to check for all changes after the event
                             // cascade, this is the best way, only consider the
                             // process if something has changed
      };
      // cout << "Process " << (*p)->name->getName() << " with " <<
      // listOfParameters.size() << "\n";

      // add processes to an event happening and remove repetitions
      for (vector< const_symbol_list * >::iterator pa =
               listOfParameters.begin();
           pa != listOfParameters.end(); ++pa) {
        if (!isProcessActive(
                *p,
                *pa) /*&& !isProcessUntriggered(*p,*pa)*/)  // no need to check
                                                            // if it has not
                                                            // been untriggered,
                                                            // because above we
                                                            // now check that
                                                            // the process is
                                                            // triggered by
                                                            // something that
                                                            // has changed
        {
          const StartAction *sa = newStartProcessAction(*p, *pa, v);
          processes.push_back(sa);
          // only add the precondition to the list of triggered processes, as we
          // already know it to be satisfied when applied
          const Proposition *prop = v->pf.buildProposition(
              (*p)->precondition, *(buildBindings(*p, **pa).copy(v)));
          activeProcesses[sa] = make_pair(prop, *pa);
          oldTriggeredEvents.push_back(sa);
          triggeredProcesses.insert(sa);
          // cout << "Triggered " << *sa << "\n";
        } else
          delete *pa;

      };  // end of looping thro' parameters

    };  // end of looping thro' processes

    // apply processes as a happening to the state
    if (processes.size() != 0) {
      if (Verbose) cout << "\n";
      ActiveCtsEffects *ace = v->getActiveCtsEffects();
      Happening *eventHappening = new Happening(v, processes, true);
      eventHappening->adjustActiveCtsEffects(*ace);
      isOK = v->executeHappening(eventHappening);
      eventHappening->clearActions();
      delete eventHappening;
      if (!isOK && !ContinueAnyway) return false;
    };

    if (EventPNEJuddering) JudderPNEs = false;
    return isOK;
  };

  const vector< const_symbol_list * > getParametersDiscreteInitialFinal(
      goal *g, operator_ *op, Validator *v) {
    vector< const_symbol_list * > aParameterList;
    const_symbol_list *blankcsl = newBlankConstSymbolList(op->parameters, v);
    aParameterList.push_back(blankcsl);
    const vector< const_symbol_list * > listOfParameters0 =
        getParametersList(g, op, v, aParameterList, false, true);
    delete blankcsl;
    const vector< const_symbol_list * > listOfParameters00 =
        removeRepeatedParameters(listOfParameters0);
    const set< var_symbol * > svs = getVariables(op);
    return defineUndefinedParameters(listOfParameters00, op, v, svs);
  };

  const vector< const_symbol_list * > getParametersDiscreteFinal(
      goal *g, operator_ *op, const State &s) {
    // get list of parameters  (may be empty)
    const vector< const_symbol_list * > listOfParameters0 =
        getParametersDiscrete(g, op, s);
    const vector< const_symbol_list * > listOfParameters00 =
        removeRepeatedParameters(listOfParameters0);
    const set< var_symbol * > svs = getVariables(op);
    return defineUndefinedParameters(listOfParameters00, op, s.getValidator(),
                                     svs);
  };

  const vector< const_symbol_list * > getParametersCtsFinal(goal *g,
                                                            operator_ *op,
                                                            Validator *v) {
    const vector< const_symbol_list * > listOfParameters0 =
        getParametersCts(g, op, v, false, false);
    const vector< const_symbol_list * > listOfParameters00 =
        removeRepeatedParameters(listOfParameters0);
    const set< var_symbol * > svs = getVariables(op);
    return defineUndefinedParameters(listOfParameters00, op, v, svs);
  };

  // trigger events given by ctsly changing PNEs
  bool Events::triggerContinuousEvents(Validator *v, bool init) {
    if (!init && v->isLastHappening()) return true;
    if (EventPNEJuddering) JudderPNEs = true;
    ctsEventTriggered = false;
    ActiveCtsEffects *ace = v->getActiveCtsEffects();
    ExecutionContext *ec = v->getExecutionContext();
    vector< const_symbol_list * > listOfParameters;

    double currentTime = v->getState().getTime();
    double nextTime;
    if (!init)
      nextTime = v->getNextHappeningTime();
    else
      nextTime = v->getCurrentHappeningTime();
    double localTime = nextTime - currentTime;
    if (localTime == 0) return true;

    bool isOK = true;
    vector< const Action * > acts;
    vector< const Action * > processes;

    ace->setLocalUpdateTime(localTime);  // set value of LocalUpdateTime - time
                                         // since last regular happening

    // process cts effects, build polys etc, conditional cts effects handled
    // here also

    if (TestingPNERobustness)
      ace->addActiveFEs(true);
    else
      ace->addActiveFEs();

    if (!ace->hasCtsEffects()) return true;

    // get parameters for all events that may be triggered due to cts effects
    for (vector< event * >::iterator e = ungroundEvents.begin();
         e != ungroundEvents.end(); ++e) {
      listOfParameters = getParametersCtsFinal((*e)->precondition, *e, v);

      for (vector< const_symbol_list * >::iterator p = listOfParameters.begin();
           p != listOfParameters.end(); ++p) {
        const Action *anAction = new Action(v, *e, *p);
        const_cast< Proposition * >(anAction->getPrecondition())
            ->setUpComparisons(ace);
        acts.push_back(anAction);
      };  // end of loop thro' parameters

      deleteParameters(listOfParameters);
    };

    // find out when events are first triggered, if at all
    vector< pair< const Action *, intervalEnd > > ctsTriggeredEvents;
    Intervals eventIntervals;
    for (vector< const Action * >::iterator e = acts.begin(); e != acts.end();
         ++e) {
      try {
        eventIntervals =
            (*e)->getPrecondition()->getIntervals(&(v->getState()));
      } catch (BadAccessError &e) {
        // if a PNE is not defined, then no problem, the event is simply not
        // triggered
      };

      if (!eventIntervals.intervals.empty()) {
        ctsTriggeredEvents.push_back(make_pair(
            *e, eventIntervals.intervals.begin()->first));  // intervals are
                                                            // constructed left
                                                            // to right so this
                                                            // is the minimum
                                                            // point
      } else
        delete *e;
    };

    // get start time for processes to trigger - add to list of actions
    map< const StartAction *, pair< const Proposition *, const_symbol_list * > >
        startProcesses;
    for (vector< process * >::iterator pro = ungroundProcesses.begin();
         pro != ungroundProcesses.end(); ++pro) {
      listOfParameters = getParametersCtsFinal((*pro)->precondition, *pro, v);

      for (vector< const_symbol_list * >::iterator p = listOfParameters.begin();
           p != listOfParameters.end(); ++p) {
        if (!isProcessActive(*pro, *p) /*&& !isProcessUntriggered(*pro,*p)*/) {
          // create a StartAction here
          const StartAction *sa = newStartProcessAction(*pro, *p, v);
          const Proposition *prop = v->pf.buildProposition(
              (*pro)->precondition, *(buildBindings(*pro, **p).copy(v)));
          const_cast< Proposition * >(prop)->setUpComparisons(ace);
          eventIntervals = prop->getIntervals(&(v->getState()));

          if (!eventIntervals.intervals.empty()) {
            intervalEnd startTime = make_pair(-1, true);

            // do not trigger a process on an isolated point
            for (vector< pair< intervalEnd, intervalEnd > >::const_iterator ei =
                     eventIntervals.intervals.begin();
                 ei != eventIntervals.intervals.end(); ++ei) {
              if (ei->first.first != ei->second.first) {
                startTime = ei->first;
                break;
              };
            };

            if (startTime.first != -1) {
              ctsTriggeredEvents.push_back(make_pair(
                  sa, startTime));  // intervals are constructed left to
                                    // right so this is the minimum point
              startProcesses[sa] = make_pair(prop, new const_symbol_list(**p));
            };
          } else {
            delete sa;
            prop->destroy();
          };
        };
      };

      deleteParameters(listOfParameters);
    };

    map< const EndAction *, const StartAction * > endStartMap;
    // find processes that could be ended
    for (map< const StartAction *,
              pair< const Proposition *, const_symbol_list * > >::iterator ap =
             activeProcesses.begin();
         ap != activeProcesses.end(); ++ap) {
      const_cast< Proposition * >(ap->second.first)->setUpComparisons(ace);
      Intervals eventIntervals0 =
          ap->second.first->getIntervals(&(v->getState()));
      eventIntervals = setComplement(eventIntervals0, localTime);
      if (!(eventIntervals.intervals.empty())) {
        const EndAction *endAct =
            newEndProcess(ap->first, ap->second.second, v);
        endStartMap[endAct] = ap->first;

        intervalEnd startTime = make_pair(-1, true);

        // do not untrigger a process on an isolated point
        for (vector< pair< intervalEnd, intervalEnd > >::const_iterator ei =
                 eventIntervals.intervals.begin();
             ei != eventIntervals.intervals.end(); ++ei) {
          if (ei->first.first != ei->second.first) {
            startTime = ei->first;
            break;
          };
        };

        if ((startTime.first != -1) && isProcessTriggered(ap->first)) {
          ctsTriggeredEvents.push_back(make_pair(endAct, startTime));
        };
      };
    };

    vector< const Action * > eventsToTrigger;
    CoScalar eventTriggerTime = 0;
    // extract the first group of events to be triggered (including processes)
    for (vector< pair< const Action *, intervalEnd > >::iterator i =
             ctsTriggeredEvents.begin();
         i != ctsTriggeredEvents.end(); ++i) {
      if (eventsToTrigger.empty()) {
        eventTriggerTime = i->second.first;
        eventsToTrigger.push_back(i->first);
      } else if (i->second.first == eventTriggerTime) {
        eventsToTrigger.push_back(i->first);
      } else if (i->second.first < eventTriggerTime) {
        eventTriggerTime = i->second.first;
        for (vector< const Action * >::iterator k = eventsToTrigger.begin();
             k != eventsToTrigger.end(); ++k)
          delete *k;
        eventsToTrigger.clear();
        eventsToTrigger.push_back(i->first);
      } else
        delete i->first;
    };

    // trigger events
    Happening *eventHappening;
    updateHappeningTime(eventTriggerTime + currentTime);
    bool triggerEventsExist = !eventsToTrigger.empty();

    // remember the no loops rule, i.e. an event cannot be triggered more than
    // once at a given time point, only the same time point as last trigger loop
    // thro' events check if they have already been triggered (unless a process)
    if (triggerEventsExist) {
      for (vector< const Action * >::const_iterator j = eventsToTrigger.begin();
           j != eventsToTrigger.end(); ++j)
        if (isTriggered(*j)) {
          if (!ContinueAnyway) return false;
          isOK = false;
        };
    };

    if (triggerEventsExist && isOK) {
      ctsEventTriggered = true;

      ace->setTime(eventTriggerTime + currentTime);  // same time as event
                                                     // trigger time
      ace->setLocalUpdateTime(eventTriggerTime);

      if (eventTriggerTime != 0) {
        // execute invariant happening
        ec->setActiveCtsEffects(ace);
        ec->setTime(eventTriggerTime + currentTime);  // same time as event
                                                      // trigger time
        if (ec->hasInvariants()) {
          if (Verbose) cout << "\n";
          isOK = v->executeHappening(ec->getInvariants()) && isOK;
        };
        ec->setTime(nextTime);  // same time as event trigger time

        // execute cts update happening
        if (Verbose) cout << "\n";
        isOK = v->executeHappening(ace->getCtsEffectUpdate()) && isOK;
      };

      // execute event happening
      if (Verbose) cout << "\n";
      eventHappening = new Happening(v, eventsToTrigger,
                                     eventTriggerTime + currentTime, true);
      eventHappening->adjustContext(*ec);
      eventHappening->adjustActiveCtsEffects(
          *ace);  // update cts effects for interval after event happening
      isOK = v->executeHappeningCtsEvent(eventHappening) && isOK;

      lastHappeningTime = eventTriggerTime + currentTime;
      vector< const StartAction * > triggeredStartProcesses;
      vector< const EndAction * > triggeredEndProcesses;
      vector< const Action * > events;

      // add to list of triggered events
      for (vector< const Action * >::const_iterator j = eventsToTrigger.begin();
           j != eventsToTrigger.end(); ++j) {
        (*j)->addTriggeredEvents(events, oldTriggeredEvents,
                                 triggeredStartProcesses,
                                 triggeredEndProcesses);
      };

      // check triggered events have falsified their preconditions and add to
      // list of triggered events
      isOK =
          checkPreconditionsAreNotSatisfied(&(v->getState()), events) && isOK;
      for (vector< const Action * >::const_iterator te = events.begin();
           te != events.end(); ++te)
        triggeredEvents.insert((*te)->getName0());

      // add triggered processes to list of triggered processes
      for (vector< const StartAction * >::const_iterator trs =
               triggeredStartProcesses.begin();
           trs != triggeredStartProcesses.end(); ++trs) {
        pair< const Proposition *, const_symbol_list * > propcsl =
            startProcesses[*trs];
        activeProcesses[*trs] = make_pair(propcsl.first, propcsl.second);
        triggeredProcesses.insert(*trs);
        startProcesses.erase(*trs);
      };

      // delete unused startProcesses' props and csls
      for (map< const StartAction *,
                pair< const Proposition *, const_symbol_list * > >::iterator
               sp = startProcesses.begin();
           sp != startProcesses.end(); ++sp) {
        sp->second.first->destroy();  // delete sp->second.first;
      };

      // remove untriggered processes from list of triggered processes
      for (vector< const EndAction * >::const_iterator trs =
               triggeredEndProcesses.begin();
           trs != triggeredEndProcesses.end(); ++trs) {
        const StartAction *stAction = endStartMap[*trs];
        map< const StartAction *,
             pair< const Proposition *, const_symbol_list * > >::iterator ap =
            activeProcesses.find(stAction);
        if (ap != activeProcesses.end()) {
          ap->second.first->destroy();
          delete ap->second.second;
          activeProcesses.erase(ap);
          untriggeredProcesses.insert(stAction->getName0());
        };
      };

      eventHappening->clearActions();
      delete eventHappening;

      // ready for triggering discrete events
      ace->setTime(nextTime);
      ace->setEventTime(eventTriggerTime + currentTime);
    } else
      for (vector< const Action * >::iterator k = eventsToTrigger.begin();
           k != eventsToTrigger.end(); ++k)
        delete *k;

    if (EventPNEJuddering) JudderPNEs = false;
    return isOK;
  };

  // for discretly triggered events
  const vector< const_symbol_list * > getParametersDiscrete(goal *g,
                                                            operator_ *op,
                                                            const State &s,
                                                            bool neg) {
    vector< const_symbol_list * > listOfparameters;

    /// Comparison
    if (const comparison *comp = dynamic_cast< const comparison * >(g)) {
      // get list of PNEs, then make list of parameter lists from them
      set< const func_term * > pnes;
      getPNEs(comp->getLHS(), pnes);
      getPNEs(comp->getRHS(), pnes);

      set< const FuncExp * > changedPNEs = s.getChangedPNEs();

      for (set< const func_term * >::iterator pne = pnes.begin();
           pne != pnes.end(); ++pne) {
        // has pne changed since last happening
        for (set< const FuncExp * >::const_iterator fe = changedPNEs.begin();
             fe != changedPNEs.end(); ++fe) {
          if (((*fe)->getName() == (*pne)->getFunction()->getName()) &&
              (*fe)->checkConstantsMatch((*pne)->getArgs()))  //+check consts
                                                              // match!
          {
            const_symbol_list *parametersForEvent = new const_symbol_list();

            for (var_symbol_list::iterator j = op->parameters->begin();
                 j != op->parameters->end(); ++j) {
              string para = getParameter(*fe, *j, *pne);

              const_symbol *cs =
                  para == ""
                      ? 0
                      : s.getValidator()->getAnalysis()->const_tab.symbol_get(
                            para);

              parametersForEvent->push_back(cs);

            };  // end of filling in parameters

            // ground out undefineds here to produce list of parameter lists
            // check the comp holds for each parameter list! use only parameters
            // used in comp
            set< var_symbol * > svs = getVariables(comp);
            listOfparameters = defineUndefinedParametersPropVar(
                parametersForEvent, op, s.getValidator(), g, false, neg, svs);
          };

        };  // end of loop for checking if pne could be a changed fe

      };  // end of looping thro' pnes in expression

      return listOfparameters;
    };

    // Literal
    if (const simple_goal *sg = dynamic_cast< const simple_goal * >(g)) {
      // handle derived predicates first!
      string literalName = sg->getProp()->head->getName();
      vector< const_symbol_list * > aParameterList;
      if (s.getValidator()->getDerivRules()->isDerivedPred(literalName)) {
        aParameterList.push_back(
            newBlankConstSymbolList(op->parameters, s.getValidator()));
        return getParametersList(g, op, s.getValidator(), aParameterList, neg,
                                 true);
      };

      // check if literal is one that has changed since last happening
      // if so fill in parameters with one from a simple prop
      set< const SimpleProposition * > changedLiterals = s.getChangedLiterals();
      for (set< const SimpleProposition * >::const_iterator sp =
               changedLiterals.begin();
           sp != changedLiterals.end(); ++sp) {
        if (((*sp)->getPropName() == literalName) &&
            ((!neg && s.evaluate(*sp)) || (neg && !s.evaluate(*sp))) &&
            (*sp)->checkConstantsMatch(sg->getProp()->args)) {
          const_symbol_list *parametersForEvent = new const_symbol_list();

          // fill in parameters for event
          for (var_symbol_list::iterator j = op->parameters->begin();
               j != op->parameters->end(); ++j) {
            string para = getParameter(*sp, *j, sg);
            const_symbol *cs =
                para == ""
                    ? 0
                    : s.getValidator()->getAnalysis()->const_tab.symbol_get(
                          para);

            parametersForEvent->push_back(cs);
          };  // end of filling in parameters

          listOfparameters.push_back(parametersForEvent);
        };
      };

      return listOfparameters;
    };

    // Negation
    if (dynamic_cast< const neg_goal * >(g)) {
      return getParametersDiscrete(
          const_cast< goal * >(dynamic_cast< const neg_goal * >(g)->getGoal()),
          op, s, !neg);
    };

    // Other
    listOfparameters = getParameters(g, op, s.getValidator(), true, neg);

    return listOfparameters;
  };

  goal *newQfiedGoal(const qfied_goal *qg, operator_ *op, Validator *v) {
    // get list of instansigated parameters for the qfied prop, so for forall(?z
    // ?y), we have a grounded list for every z? and ?y
    set< var_symbol * > svs = getVariables(qg);
    vector< const_symbol_list * > constantsList = defineUndefinedParameters(
        newBlankConstSymbolList(const_cast< var_symbol_list * >(qg->getVars()),
                                v),
        const_cast< var_symbol_list * >(qg->getVars()), v, svs);

    // now create a conjunction or disjunction with the qfied variables
    // substituted
    map< parameter_symbol *, parameter_symbol * > newvars;
    goal_list *theGoals = new goal_list();

    for (vector< const_symbol_list * >::iterator k = constantsList.begin();
         k != constantsList.end(); ++k) {
      const goal *aGoal = copyGoal(qg->getGoal());

      // define mapping of parameter symbol to constant
      const_symbol_list::iterator consList = (*k)->begin();
      for (var_symbol_list::const_iterator i = qg->getVars()->begin();
           i != qg->getVars()->end(); ++i) {
        newvars[const_cast< var_symbol * >(*i)] = *consList;
        consList++;
      };
      // add conjunct/disjunct with qfied variables substituted
      changeVars(const_cast< goal * >(aGoal), newvars);
      theGoals->push_back(const_cast< goal * >(aGoal));
    };

    deleteParameters(constantsList);

    goal *goalToCheck;
    if (qg->getQuantifier() == E_FORALL) {
      goalToCheck = new conj_goal(theGoals);
    } else {
      goalToCheck = new disj_goal(theGoals);
    };

    return goalToCheck;
  };

  // for ctsly triggered events
  const vector< const_symbol_list * > getParametersCts(goal *g, operator_ *op,
                                                       Validator *v, bool neg,
                                                       bool atAPoint) {
    vector< const_symbol_list * > listOfparameters;
    vector< const_symbol_list * > alistOfparameters;

    /// Comparison
    if (const comparison *comp = dynamic_cast< const comparison * >(g)) {
      // get list of PNEs, then make list of parameter lists from them
      set< const func_term * > pnes;
      getPNEs(comp->getLHS(), pnes);
      getPNEs(comp->getRHS(), pnes);

      for (set< const func_term * >::iterator pne = pnes.begin();
           pne != pnes.end(); ++pne) {
        // loop thro' ctsly changing PNEs
        for (map< const FuncExp *, ActiveFE * >::const_iterator fe =
                 v->getActiveCtsEffects()->activeFEs.begin();
             fe != v->getActiveCtsEffects()->activeFEs.end(); ++fe) {
          if (fe->first->getName() == (*pne)->getFunction()->getName() &&
              fe->first->checkConstantsMatch((*pne)->getArgs())) {
            const_symbol_list *parametersForEvent = new const_symbol_list();

            // fill in parameters for event
            for (var_symbol_list::iterator j = op->parameters->begin();
                 j != op->parameters->end(); ++j) {
              string para = getParameter(fe->first, *j, *pne);
              const_symbol *cs =
                  para == "" ? 0 : v->getAnalysis()->const_tab.symbol_get(para);

              parametersForEvent->push_back(cs);
            };  // end of filling in parameters

            // any undefined parameters will be ground out and checked later,
            // unless we are checking at a point for mutex checks with actions
            // at the same time.
            if (!atAPoint)
              listOfparameters.push_back(parametersForEvent);
            else {
              set< var_symbol * > svs = getVariables(comp);
              alistOfparameters = defineUndefinedParametersPropVar(
                  parametersForEvent, op, v, g, false, neg, svs, true);

              for (vector< const_symbol_list * >::const_iterator l =
                       alistOfparameters.begin();
                   l != alistOfparameters.end(); ++l)
                listOfparameters.push_back(*l);
            };
          };

        };  // end of loop for checking if pne could be a changed fe

      };  // end of looping thro' pnes in expression

      return listOfparameters;
    };

    // Literal
    if (dynamic_cast< const simple_goal * >(g)) {
      // return an empty list, literals do not change ctsly, so cannot trigger a
      // event by cts activity
      return listOfparameters;
    };

    // Negation
    if (dynamic_cast< const neg_goal * >(g)) {
      return getParametersCts(
          const_cast< goal * >(dynamic_cast< const neg_goal * >(g)->getGoal()),
          op, v, !neg, atAPoint);
    };

    // Others
    listOfparameters = getParameters(g, op, v, false, neg, atAPoint);

    return listOfparameters;
  };

  // for both discrete and cts
  const vector< const_symbol_list * > getParameters(goal *g, operator_ *op,
                                                    Validator *v, bool discrete,
                                                    bool neg, bool atAPoint) {
    vector< const_symbol_list * > listOfparameters;

    /// Conjunction
    if ((!neg && (dynamic_cast< const conj_goal * >(g))) ||
        (neg && (dynamic_cast< const disj_goal * >(g)))) {
      const goal_list *goalList;
      if (dynamic_cast< const conj_goal * >(g)) {
        goalList = dynamic_cast< const conj_goal * >(g)->getGoals();
      } else {
        goalList = dynamic_cast< const disj_goal * >(g)->getGoals();
      };

      // loop thro' conjuncts
      // get all parameters from each
      for (pc_list< goal * >::const_iterator i = goalList->begin();
           i != goalList->end(); ++i) {
        vector< const_symbol_list * > someParameters;
        if (discrete)
          someParameters = getParametersDiscrete(*i, op, v->getState(), neg);
        else
          someParameters = getParametersCts(*i, op, v, neg, atAPoint);

        // whittle down the list of parameters depending if they satisfy the
        // rest of the conjunction
        vector< const_symbol_list * > alistOfparameters;
        if (!someParameters.empty())
          alistOfparameters = getParametersList(g, op, v, someParameters, neg,
                                                discrete, atAPoint);
        deleteParameters(someParameters);

        for (vector< const_symbol_list * >::const_iterator l =
                 alistOfparameters.begin();
             l != alistOfparameters.end(); ++l)
          listOfparameters.push_back(*l);
      };

      return listOfparameters;
    };

    /// Disjunction
    if ((!neg && (dynamic_cast< const disj_goal * >(g))) ||
        (neg && (dynamic_cast< const conj_goal * >(g)))) {
      const goal_list *goalList;
      if (dynamic_cast< const disj_goal * >(g)) {
        goalList = dynamic_cast< const disj_goal * >(g)->getGoals();
      } else {
        goalList = dynamic_cast< const conj_goal * >(g)->getGoals();
      };
      // loop thro' disjuncts
      for (pc_list< goal * >::const_iterator i = goalList->begin();
           i != goalList->end(); ++i) {
        vector< const_symbol_list * > someParameters;
        if (discrete)
          someParameters = getParametersDiscrete(*i, op, v->getState(), neg);
        else
          someParameters = getParametersCts(*i, op, v, neg, atAPoint);

        for (vector< const_symbol_list * >::const_iterator l =
                 someParameters.begin();
             l != someParameters.end(); ++l)
          listOfparameters.push_back(*l);
        // All remaining undefineds are given by existing objects and could be
        // anything since remaining disjuncts need not be satisfied - thus leave
        // as undefined
      };

      return listOfparameters;
    };

    if (const qfied_goal *qg = dynamic_cast< const qfied_goal * >(g)) {
      goal *goalToCheck = newQfiedGoal(qg, op, v);

      if (discrete)
        listOfparameters =
            getParametersDiscrete(goalToCheck, op, v->getState(), neg);
      else
        listOfparameters = getParametersCts(goalToCheck, op, v, neg, atAPoint);

      delete goalToCheck;

      return listOfparameters;
    };

    if (const imply_goal *ig = dynamic_cast< const imply_goal * >(g)) {
      neg_goal *ng = new neg_goal(const_cast< goal * >(ig->getAntecedent()));
      goal_list *gl = new goal_list();
      ;
      goal *agoal = new goal(*const_cast< goal * >(ig->getConsequent()));
      gl->push_back(ng);
      gl->push_back(agoal);
      disj_goal *goalToCheck = new disj_goal(gl);

      if (discrete)
        listOfparameters =
            getParametersDiscrete(goalToCheck, op, v->getState(), neg);
      else
        listOfparameters = getParametersCts(goalToCheck, op, v, neg, atAPoint);
      gl->clear();
      ng->destroy();
      delete agoal;
      delete goalToCheck;

      return listOfparameters;
    };

    return listOfparameters;
  };

  void unionVariables(set< var_symbol * > &svs1, set< var_symbol * > &svs2) {
    for (set< var_symbol * >::const_iterator i = svs2.begin(); i != svs2.end();
         ++i) {
      svs1.insert(*i);
    };
  };

  // does the goal contain a negation or a comparsion?
  bool containsNegationComp(goal *g, bool neg) {
    if (dynamic_cast< const comparison * >(g)) {
      return true;
    };

    if (const conj_goal *cg = dynamic_cast< const conj_goal * >(g)) {
      for (pc_list< goal * >::const_iterator i = cg->getGoals()->begin();
           i != cg->getGoals()->end(); ++i) {
        if (containsNegationComp(*i, neg)) return true;
      };
      return false;
    };

    if (const disj_goal *dg = dynamic_cast< const disj_goal * >(g)) {
      for (pc_list< goal * >::const_iterator i = dg->getGoals()->begin();
           i != dg->getGoals()->end(); ++i) {
        if (containsNegationComp(*i, neg)) return true;
      };
      return false;
    };

    if (const neg_goal *ng = dynamic_cast< const neg_goal * >(g)) {
      return containsNegationComp(const_cast< goal * >(ng->getGoal()), !neg);
    };

    if (const imply_goal *ig = dynamic_cast< const imply_goal * >(g)) {
      return containsNegationComp(const_cast< goal * >(ig->getAntecedent()),
                                  neg) ||
             containsNegationComp(const_cast< goal * >(ig->getConsequent()),
                                  neg);
    };

    if (dynamic_cast< const simple_goal * >(g)) {
      return neg;
    };

    if (const qfied_goal *qg = dynamic_cast< const qfied_goal * >(g)) {
      return containsNegationComp(const_cast< goal * >(qg->getGoal()), neg);
    };

    return false;
  };

  const vector< const_symbol_list * > getCopyCSL(
      const vector< const_symbol_list * > &lop) {
    vector< const_symbol_list * > listOfparameters;

    for (vector< const_symbol_list * >::const_iterator p = lop.begin();
         p != lop.end(); ++p) {
      listOfparameters.push_back(new const_symbol_list(**p));
    };

    return listOfparameters;
  };

  // find the list of parameters lists that satisfy g from the given list of
  // parameter lists lop (psi as in paper)
  const vector< const_symbol_list * > getParametersList(
      goal *g, operator_ *op, Validator *v,
      const vector< const_symbol_list * > &lop, bool neg, bool discrete,
      bool atAPoint) {
    vector< const_symbol_list * > listOfparameters;

    /// Comparison
    if (const comparison *comp = dynamic_cast< const comparison * >(g)) {
      // if checking for ctsly triggered events we need to assume any comps with
      // ctsly changing pnes are true at this stage. The comps are checked
      // later, so do not do any checking here, it is done later (which will
      // also include any comps with no ctsly changing PNEs that may be given
      // here)
      if (!discrete && !atAPoint) {
        // get list of PNEs, then make list of parameter lists from them
        set< const func_term * > pnes;
        getPNEs(comp->getLHS(), pnes);
        getPNEs(comp->getRHS(), pnes);
        bool hasCtsPNE = false;

        for (set< const func_term * >::iterator pne = pnes.begin();
             pne != pnes.end(); ++pne) {
          // loop thro' ctsly changing PNEs
          for (map< const FuncExp *, ActiveFE * >::const_iterator fe =
                   v->getActiveCtsEffects()->activeFEs.begin();
               fe != v->getActiveCtsEffects()->activeFEs.end(); ++fe) {
            if (fe->first->getName() == (*pne)->getFunction()->getName()) {
              hasCtsPNE = true;
            };

          };  // end of loop for checking if pne could be a changed fe

        };  // end of looping thro' pnes in expression

        // return copy of lop
        if (hasCtsPNE) {
          return getCopyCSL(lop);
        };
      };

      // get list of unique parameters from g
      set< var_symbol * > svs = getVariables(comp->getLHS());
      set< var_symbol * > svs2 = getVariables(comp->getRHS());
      unionVariables(svs, svs2);

      // dont want to delete lop
      vector< const_symbol_list * > someParameters;
      for (vector< const_symbol_list * >::const_iterator p = lop.begin();
           p != lop.end(); ++p) {
        someParameters.push_back(new const_symbol_list(**p));
      };
      vector< const_symbol_list * > listOfparameters =
          defineUndefinedParametersPropVar(someParameters, op, v, g, false, neg,
                                           svs, atAPoint);

      return listOfparameters;
    };

    // Literal
    if (const simple_goal *sg = dynamic_cast< const simple_goal * >(g)) {
      // look in state, look up all simple props that are true with this name.
      // Get a list of constant symbols corresponding to the true literals.
      // Create a list of partially ground parameters from these and lop
      string literalName = sg->getProp()->head->getName();
      bool isDerivedPred = v->getDerivRules()->isDerivedPred(literalName);

      LogicalState logState = v->getState().getLogicalState();
      if (!neg && !isDerivedPred) {
        for (LogicalState::const_iterator i = logState.begin();
             i != logState.end(); ++i) {
          if (i->second && (i->first->getPropName() == literalName)) {
            if (i->first->checkParametersConstantsMatch(sg->getProp()->args)) {
              addToListOfParameters(
                  listOfparameters, lop,
                  i->first->getConstants(op->parameters, sg->getProp()->args,
                                         v));
            }
          };
        };
      } else {
        // old style method for negations and derived predicates
        set< var_symbol * > svs = getVariables(sg);
        vector< const_symbol_list * > someParameters;
        for (vector< const_symbol_list * >::const_iterator p = lop.begin();
             p != lop.end(); ++p) {
          someParameters.push_back(new const_symbol_list(**p));
        };
        listOfparameters = defineUndefinedParametersPropVar(
            someParameters, op, v, g, isDerivedPred, neg, svs);
      };
      return listOfparameters;
    };

    // Negation
    if (dynamic_cast< const neg_goal * >(g)) {
      return getParametersList(
          const_cast< goal * >(dynamic_cast< const neg_goal * >(g)->getGoal()),
          op, v, lop, !neg, discrete, atAPoint);
    };

    /// Conjunction
    if ((!neg && (dynamic_cast< const conj_goal * >(g))) ||
        (neg && (dynamic_cast< const disj_goal * >(g)))) {
      const goal_list *goalList;
      if (dynamic_cast< const conj_goal * >(g)) {
        goalList = dynamic_cast< const conj_goal * >(g)->getGoals();
      } else {
        goalList = dynamic_cast< const disj_goal * >(g)->getGoals();
      };

      if (goalList->empty()) return getCopyCSL(lop);

      vector< const_symbol_list * > aListOfparameters;
      vector< const_symbol_list * > aListOfparametersTemp;
      for (vector< const_symbol_list * >::const_iterator p = lop.begin();
           p != lop.end(); ++p)
        aListOfparametersTemp.push_back(new const_symbol_list(**p));

      vector< goal * > negCompGoals;  // do negative ones (and comparisons)
                                      // later as these often cause a lot of
                                      // work, try to reduce list first
      // loop thro' conjuncts
      for (pc_list< goal * >::const_iterator i = goalList->begin();
           i != goalList->end(); ++i) {
        if (containsNegationComp(*i, neg))
          negCompGoals.push_back(*i);
        else {
          // get the list of parameters for each conjunct and then pass on list
          // for next conjunct
          if (!aListOfparametersTemp.empty()) {
            aListOfparameters = getParametersList(
                *i, op, v, aListOfparametersTemp, neg, discrete,
                atAPoint);  // cout << " size of temp =
                            // "<<aListOfparameters.size()<<"\n";
            deleteParameters(aListOfparametersTemp);
            aListOfparametersTemp = aListOfparameters;
          };
        };
      };

      for (vector< goal * >::const_iterator j = negCompGoals.begin();
           j != negCompGoals.end(); ++j) {
        if (!aListOfparametersTemp.empty()) {
          aListOfparameters = getParametersList(
              *j, op, v, aListOfparametersTemp, neg, discrete,
              atAPoint);  // cout << " size of temp =
                          // "<<aListOfparameters.size()<<"\n";
          deleteParameters(aListOfparametersTemp);
          aListOfparametersTemp = aListOfparameters;
        };
      };

      // maybe be some undefined parameters left over

      return aListOfparameters;
    };

    /// Disjunction
    if ((!neg && (dynamic_cast< const disj_goal * >(g))) ||
        (neg && (dynamic_cast< const conj_goal * >(g)))) {
      const goal_list *goalList;
      if (dynamic_cast< const disj_goal * >(g)) {
        goalList = dynamic_cast< const disj_goal * >(g)->getGoals();
      } else {
        goalList = dynamic_cast< const conj_goal * >(g)->getGoals();
      };
      // loop thro' disjuncts
      for (pc_list< goal * >::const_iterator i = goalList->begin();
           i != goalList->end(); ++i) {
        vector< const_symbol_list * > someParameters;
        someParameters =
            getParametersList(*i, op, v, lop, neg, discrete, atAPoint);
        for (vector< const_symbol_list * >::iterator j = someParameters.begin();
             j != someParameters.end(); ++j)
          listOfparameters.push_back(*j);

        // All remaining undefineds are given by existing objects and could be
        // anything since remaining disjuncts need not be satisfied - thus leave
        // as undefined
      };

      return listOfparameters;
    };

    if (const qfied_goal *qg = dynamic_cast< const qfied_goal * >(g)) {
      goal *goalToCheck = newQfiedGoal(qg, op, v);

      listOfparameters =
          getParametersList(goalToCheck, op, v, lop, neg, discrete, atAPoint);

      delete goalToCheck;

      return listOfparameters;
    };

    if (const imply_goal *ig = dynamic_cast< const imply_goal * >(g)) {
      neg_goal *ng = new neg_goal(const_cast< goal * >(ig->getAntecedent()));
      goal_list *gl = new goal_list();
      ;
      goal *agoal = new goal(*const_cast< goal * >(ig->getConsequent()));
      gl->push_back(ng);
      gl->push_back(agoal);
      disj_goal *goalToCheck = new disj_goal(gl);

      listOfparameters =
          getParametersList(goalToCheck, op, v, lop, neg, discrete, atAPoint);
      gl->clear();
      ng->destroy();
      delete agoal;
      delete goalToCheck;

      return listOfparameters;
    };

    return listOfparameters;
  };

  // find vs in the simple_goal parameters, map this to the parameter
  // instantigation in sp
  string getParameter(const SimpleProposition *sp, var_symbol *vs,
                      const simple_goal *sg) {
    string parameterName = "";
    int parameterNo = 1;
    parameter_symbol_list::iterator p = sg->getProp()->args->begin();
    for (; p != sg->getProp()->args->end(); ++p) {
      if (vs == *p) break;
      ++parameterNo;
    };

    if (p != sg->getProp()->args->end()) {
      parameterName = sp->getParameter(parameterNo);
    };

    return parameterName;
  };

  // find vs in the func_term parameters, map this to the parameter
  // instantigation in fe
  string getParameter(const FuncExp *fe, var_symbol *vs, const func_term *pne) {
    string parameterName = "";
    int parameterNo = 1;
    parameter_symbol_list *psl =
        const_cast< parameter_symbol_list * >(pne->getArgs());
    parameter_symbol_list::iterator p = psl->begin();
    for (; p != psl->end(); ++p) {
      if (vs == *p) break;
      ++parameterNo;
    };

    if (p != psl->end()) {
      parameterName = fe->getParameter(parameterNo);
    };

    return parameterName;
  };

  bool undefinedParameterExists(const_symbol_list *csl) {
    for (const_symbol_list::iterator cs = csl->begin(); cs != csl->end();
         ++cs) {
      if (!(*cs)) return true;
    };

    return false;
  };

  const set< var_symbol * > getVariables(const expression *e) {
    set< var_symbol * > theVariables;

    if (dynamic_cast< const binary_expression * >(e)) {
      const binary_expression *be =
          dynamic_cast< const binary_expression * >(e);
      theVariables = getVariables(be->getLHS());
      set< var_symbol * > svs2 = getVariables(be->getRHS());
      unionVariables(theVariables, svs2);
      return theVariables;
    };

    if (dynamic_cast< const uminus_expression * >(e)) {
      const uminus_expression *ue =
          dynamic_cast< const uminus_expression * >(e);
      theVariables = getVariables(ue->getExpr());
      return theVariables;
    };

    if (const func_term *fe = dynamic_cast< const func_term * >(e)) {
      parameter_symbol_list *param_list =
          const_cast< parameter_symbol_list * >(fe->getArgs());

      for (parameter_symbol_list::iterator i = param_list->begin();
           i != param_list->end(); ++i) {
        if (dynamic_cast< const var_symbol * >(*i)) {
          theVariables.insert(const_cast< var_symbol * >(
              dynamic_cast< const var_symbol * >(*i)));
        };
      };
    };

    return theVariables;
  };

  const set< var_symbol * > getVariables(const simple_goal *sg) {
    set< var_symbol * > theVariables;

    for (parameter_symbol_list::iterator i = sg->getProp()->args->begin();
         i != sg->getProp()->args->end(); ++i) {
      if (dynamic_cast< const var_symbol * >(*i)) {
        theVariables.insert(
            const_cast< var_symbol * >(dynamic_cast< const var_symbol * >(*i)));
      };
    };

    return theVariables;
  };

  const set< var_symbol * > getVariables(const qfied_goal *qg) {
    set< var_symbol * > theVariables;

    for (var_symbol_list::const_iterator i = qg->getVars()->begin();
         i != qg->getVars()->end(); ++i) {
      theVariables.insert(const_cast< var_symbol * >(*i));
    };

    return theVariables;
  };

  const set< var_symbol * > getVariables(const operator_ *op) {
    set< var_symbol * > theVariables;

    for (var_symbol_list::const_iterator i = op->parameters->begin();
         i != op->parameters->end(); ++i) {
      theVariables.insert(*i);
    };

    return theVariables;
  };

  // fill in parameters in lop with those in csl and return results, discard csl
  // also
  void addToListOfParameters(vector< const_symbol_list * > &vcsl,
                             const vector< const_symbol_list * > &lop,
                             const_symbol_list *csl) {
    bool satisfied;

    for (vector< const_symbol_list * >::const_iterator i = lop.begin();
         i != lop.end(); ++i) {
      const_symbol_list *aConstList = new const_symbol_list(**i);

      satisfied = true;
      const_symbol_list::const_iterator j = csl->begin();
      const_symbol_list::iterator l = aConstList->begin();
      for (const_symbol_list::const_iterator k = (*i)->begin();
           k != (*i)->end(); ++k) {
        if ((*j)) {
          if (!(*k))
            *l = *j;
          else if (*l != *j)
            satisfied =
                false;  // the literal(or other) is not satisfied by previously
                        // defined parameters so not add to list of parameters
        };

        ++j;
        ++l;
      };

      if (satisfied)
        vcsl.push_back(aConstList);
      else
        delete aConstList;
    };

    delete csl;

    // test
    /*      cout << " results\n";
          for(vector<const_symbol_list*>::const_iterator k = vcsl.begin(); k !=
       vcsl.end() ; ++k)
          {
             for(const_symbol_list::iterator l = (*k)->begin(); l !=
       (*k)->end();
       ++l)
             {
               cout << (*l)->getName();

             };
             cout <<"\n";
          }; */
    // end test
  };

  // for function below
  bool isInList(const set< var_symbol * > &svs, var_symbol *vs) {
    set< var_symbol * >::const_iterator i = svs.find(vs);
    return (i != svs.end());
  };

  // returns new set of parameter lists based on csl, only defines undefined
  // variables if they are in svs
  const vector< const_symbol_list * > defineUndefinedParameters(
      const_symbol_list *csl, var_symbol_list *variables, Validator *vld,
      const set< var_symbol * > &svs) {
    map< unsigned int, const_symbol_list * > definedLists;
    vector< const_symbol_list * > finalDefinedLists;

    if (csl->size() == 0 || !undefinedParameterExists(csl)) {
      finalDefinedLists.push_back(new const_symbol_list(*csl));
      delete csl;

      return finalDefinedLists;
    };

    definedLists[1] = new const_symbol_list(*csl);
    const_symbol_list *considerList = definedLists[1];
    unsigned int definedListNoConsider = 0;
    unsigned int definedListNoAdd = 1;

    // loop thro definedLists until every parameter is ground, adding to
    // definedLists when grounding a variable and other undefineds remain

    int paraNumber;
    int paraNumber0;
    bool remainingParasDefined;

    do {
      ++definedListNoConsider;
      map< unsigned int, const_symbol_list * >::iterator dl =
          definedLists.find(definedListNoConsider);
      if (dl == definedLists.end()) break;
      considerList = dl->second;

      // choose the first undefined parameter
      const_symbol_list::iterator cs = considerList->begin();
      var_symbol_list::iterator vs = variables->begin();
      paraNumber = 1;
      for (; cs != considerList->end(); ++cs) {
        if (!(*cs) && isInList(svs, *vs)) break;
        ++vs;
        ++paraNumber;
      };

      if (cs == considerList->end()) {
        delete considerList;
        break;
      };

      // are remaining parameters defined in list?
      remainingParasDefined = true;
      var_symbol_list::iterator vs0 = variables->begin();
      paraNumber0 = 1;
      for (const_symbol_list::iterator cs0 = considerList->begin();
           cs0 != considerList->end(); ++cs0) {
        if ((!(*cs0)) && isInList(svs, *vs0) && (paraNumber0 > paraNumber))
          remainingParasDefined = false;
        ++vs0;
        ++paraNumber0;
      };

      // define the parameter for every possibility and add to list of
      // definedLists
      // cout << "Seeking range for " << **vs << "\n";
      vector< const_symbol * > vals = vld->range(*vs);
      // cout << "Got\n";
      for (vector< const_symbol * >::const_iterator obj = vals.begin();
           obj != vals.end(); ++obj) {
        const_symbol_list *parameters = new const_symbol_list(*considerList);

        const_symbol_list::iterator j = parameters->begin();
        for (int k = 1; k < paraNumber; ++k) {
          ++j;
        };
        *j = *obj;

        if (!remainingParasDefined)
          definedLists[++definedListNoAdd] = parameters;
        else
          finalDefinedLists.push_back(parameters);
      };

      delete considerList;  // delete each consider list
    } while (true);  // end of looping thro defined lists, for given parameter,
                     // move to next parameter if considered parameter set was
                     // last in list when chosen

    /*
    if(finalDefinedLists.empty())
    {
      finalDefinedLists.push_back(new const_symbol_list(*csl));
    };
    */
    // test
    /*  cout << finalDefinedLists.size() << " results\n";

      for(vector<const_symbol_list*>::const_iterator k =
      finalDefinedLists.begin(); k != finalDefinedLists.end() ; ++k)
      {
         for(const_symbol_list::iterator l = (*k)->begin(); l != (*k)->end();
      ++l)
         {
           cout << (*l)->getName();

         };
         cout <<"\n";
      };  //end test
      */

    delete csl;
    return finalDefinedLists;
  };

  const vector< const_symbol_list * > defineUndefinedParameters(
      const vector< const_symbol_list * > &vcsl, operator_ *op, Validator *vld,
      const set< var_symbol * > &svs) {
    vector< const_symbol_list * > definedLists;
    vector< const_symbol_list * > someDefinedLists;

    for (vector< const_symbol_list * >::const_iterator csl = vcsl.begin();
         csl != vcsl.end(); ++csl) {
      someDefinedLists =
          defineUndefinedParameters(*csl, op->parameters, vld, svs);

      for (vector< const_symbol_list * >::const_iterator i =
               someDefinedLists.begin();
           i != someDefinedLists.end(); ++i)
        definedLists.push_back(*i);
    };

    return definedLists;
  };

  // return parameter lists such that they satisfy the goal g, also delete
  // reject candidate parameter lists!
  const vector< const_symbol_list * > checkParametersProp(
      const vector< const_symbol_list * > &vcsl, operator_ *op, Validator *vld,
      goal *g, bool neg, bool dp, bool compError) {
    vector< const_symbol_list * > definedLists;

    for (vector< const_symbol_list * >::const_iterator gp = vcsl.begin();
         gp != vcsl.end(); ++gp) {
      bool propSatisfied;
      if (dynamic_cast< const simple_goal * >(g) && !dp) {
        const Proposition *prop =
            vld->pf.buildProposition(g, *(buildBindings(op, **gp).copy(vld)));
        propSatisfied = prop->evaluate(&vld->getState());
        prop->destroy();
      } else {
        const Proposition *prop =
            vld->pf.buildProposition(g, *(buildBindings(op, **gp).copy(vld)));
        try {
          if (compError)
            propSatisfied = prop->evaluateAtPointWithinError(&vld->getState());
          else
            propSatisfied = prop->evaluate(&vld->getState());
        } catch (BadAccessError &e) {
          if (!neg)
            propSatisfied = false;
          else
            propSatisfied = true;  // if a PNE is not defined, then no problem,
                                   // the event is simply not triggered
        };
        prop->destroy();
      };

      if ((propSatisfied && !neg) || (!propSatisfied && neg)) {
        definedLists.push_back(*gp);
      } else
        delete *gp;
    };

    return definedLists;
  };

  // define undefined parameters in csl (but only if in svs!) and ensure they
  // satisfy the goal of the event
  const vector< const_symbol_list * > defineUndefinedParametersPropVar(
      const_symbol_list *csl, operator_ *op, Validator *vld, goal *g, bool dp,
      bool neg, const set< var_symbol * > &svs, bool compError) {
    vector< const_symbol_list * > groundListOfParameters;

    // if there are variables to ground then ground 'em!
    if (!svs.empty())
      groundListOfParameters =
          defineUndefinedParameters(csl, op->parameters, vld, svs);
    else {
      groundListOfParameters.push_back(new const_symbol_list(*csl));
      delete csl;
    };

    return checkParametersProp(groundListOfParameters, op, vld, g, neg, dp,
                               compError);
  };

  const vector< const_symbol_list * > defineUndefinedParametersPropVar(
      const vector< const_symbol_list * > &vcsl, operator_ *op, Validator *vld,
      goal *g, bool dp, bool neg, const set< var_symbol * > &svs,
      bool compError) {
    vector< const_symbol_list * > definedLists;
    vector< const_symbol_list * > someDefinedLists;

    for (vector< const_symbol_list * >::const_iterator csl = vcsl.begin();
         csl != vcsl.end(); ++csl) {
      someDefinedLists = defineUndefinedParametersPropVar(*csl, op, vld, g, dp,
                                                          neg, svs, compError);

      for (vector< const_symbol_list * >::const_iterator i =
               someDefinedLists.begin();
           i != someDefinedLists.end(); ++i)
        definedLists.push_back(*i);
    };

    return definedLists;
  };

  // get pnes in expression e
  void getPNEs(const expression *e, set< const func_term * > &pnes) {
    if (const func_term *fexpression = dynamic_cast< const func_term * >(e)) {
      pnes.insert(fexpression);
      return;
    };

    if (const binary_expression *bexp =
            dynamic_cast< const binary_expression * >(e)) {
      getPNEs(bexp->getLHS(), pnes);
      getPNEs(bexp->getRHS(), pnes);
      return;
    };

    if (const uminus_expression *uexp =
            dynamic_cast< const uminus_expression * >(e)) {
      getPNEs(uexp->getExpr(), pnes);
    };
  };

  // copy a goal including all subgoals
  const goal *copyGoal(const goal *g) {
    if (dynamic_cast< const neg_goal * >(g)) {
      const goal *ng = (dynamic_cast< const neg_goal * >(g))->getGoal();

      return new neg_goal(const_cast< goal * >(copyGoal(ng)));
    };

    if (dynamic_cast< const imply_goal * >(g)) {
      const imply_goal *ig = dynamic_cast< const imply_goal * >(g);

      neg_goal *ng =
          new neg_goal(const_cast< goal * >(copyGoal(ig->getAntecedent())));
      goal_list *gl = new goal_list();
      ;
      goal *agoal = const_cast< goal * >(copyGoal(ig->getConsequent()));
      gl->push_back(ng);
      gl->push_back(agoal);
      const disj_goal *dg = new disj_goal(gl);

      return copyGoal(dg);
    };

    if (dynamic_cast< const conj_goal * >(g)) {
      const conj_goal *cg = dynamic_cast< const conj_goal * >(g);
      goal_list *gl = new goal_list();
      for (pc_list< goal * >::const_iterator i = cg->getGoals()->begin();
           i != cg->getGoals()->end(); ++i) {
        gl->push_back(const_cast< goal * >(copyGoal(*i)));
      };
      return new conj_goal(gl);
    };

    if (dynamic_cast< const disj_goal * >(g)) {
      const disj_goal *dg = dynamic_cast< const disj_goal * >(g);
      goal_list *gl = new goal_list();
      for (pc_list< goal * >::const_iterator i = dg->getGoals()->begin();
           i != dg->getGoals()->end(); ++i) {
        gl->push_back(const_cast< goal * >(copyGoal(*i)));
      };
      const disj_goal *d_goal = new disj_goal(gl);

      return d_goal;
    };

    if (dynamic_cast< const qfied_goal * >(g)) {
      const qfied_goal *qg = dynamic_cast< const qfied_goal * >(g);

      const qfied_goal *ans;
      var_symbol_table *sym_tab = new var_symbol_table();
      for (map< string, var_symbol * >::const_iterator i =
               qg->getSymTab()->begin();
           i != qg->getSymTab()->end(); ++i) {
        sym_tab->symbol_put(i->first);
      };

      if (qg->getQuantifier() == E_EXISTS)
        ans = new qfied_goal(
            E_EXISTS,
            new var_symbol_list(
                *const_cast< var_symbol_list * >(qg->getVars())),
            const_cast< goal * >(copyGoal(const_cast< goal * >(qg->getGoal()))),
            sym_tab);
      else
        ans = new qfied_goal(
            E_FORALL,
            new var_symbol_list(
                *const_cast< var_symbol_list * >(qg->getVars())),
            const_cast< goal * >(copyGoal(const_cast< goal * >(qg->getGoal()))),
            sym_tab);

      return ans;
    };

    if (dynamic_cast< const simple_goal * >(g)) {
      const simple_goal *sg = dynamic_cast< const simple_goal * >(g);
      parameter_symbol_list *newpsl = new parameter_symbol_list();
      for (parameter_symbol_list::iterator i = sg->getProp()->args->begin();
           i != sg->getProp()->args->end(); ++i) {
        newpsl->push_back(*i);
      };
      const proposition *prop = new proposition(sg->getProp()->head, newpsl);
      const simple_goal *sim_goal =
          new simple_goal(const_cast< proposition * >(prop), sg->getPolarity());

      return sim_goal;
    };

    if (dynamic_cast< const comparison * >(g)) {
      const comparison *comp = dynamic_cast< const comparison * >(g);
      const expression *e1 = copyExpression(comp->getLHS());  // copy
      const expression *e2 = copyExpression(comp->getRHS());

      return new comparison(comp->getOp(), const_cast< expression * >(e1),
                            const_cast< expression * >(e2));
    };

    return g;
  };

  const expression *copyExpression(const expression *e) {
    if (const div_expression *fexpression =
            dynamic_cast< const div_expression * >(e)) {
      return new div_expression(
          const_cast< expression * >(copyExpression(fexpression->getLHS())),
          const_cast< expression * >(copyExpression(fexpression->getRHS())));
    };

    if (const minus_expression *fexpression =
            dynamic_cast< const minus_expression * >(e)) {
      return new minus_expression(
          const_cast< expression * >(copyExpression(fexpression->getLHS())),
          const_cast< expression * >(copyExpression(fexpression->getRHS())));
    };

    if (const mul_expression *fexpression =
            dynamic_cast< const mul_expression * >(e)) {
      return new mul_expression(
          const_cast< expression * >(copyExpression(fexpression->getLHS())),
          const_cast< expression * >(copyExpression(fexpression->getRHS())));
    };

    if (const plus_expression *fexpression =
            dynamic_cast< const plus_expression * >(e)) {
      return new plus_expression(
          const_cast< expression * >(copyExpression(fexpression->getLHS())),
          const_cast< expression * >(copyExpression(fexpression->getRHS())));
    };

    if (const int_expression *fexpression =
            dynamic_cast< const int_expression * >(e)) {
      int aNumber = int(fexpression->double_value());
      return new int_expression(aNumber);
    };

    if (const float_expression *fexpression =
            dynamic_cast< const float_expression * >(e)) {
      NumScalar aNumber = fexpression->double_value();
      return new float_expression(aNumber);
    };

    if (const uminus_expression *fexpression =
            dynamic_cast< const uminus_expression * >(e)) {
      return new uminus_expression(
          const_cast< expression * >(copyExpression(fexpression->getExpr())));
    };

    if (const func_term *fexpression = dynamic_cast< const func_term * >(e)) {
      parameter_symbol_list *newpsl = new parameter_symbol_list();
      for (parameter_symbol_list::const_iterator i =
               fexpression->getArgs()->begin();
           i != fexpression->getArgs()->end(); ++i) {
        newpsl->push_back(*i);
      };

      return new func_term(
          const_cast< func_symbol * >(fexpression->getFunction()), newpsl);
    };

    if (dynamic_cast< const special_val_expr * >(e)) {
      return e;
    };

    return e;
  };

};  // namespace VAL
